The present invention relates to a method and a system for verifying the equivalence of digital circuit designs.
Logic Design Verification
Digital logic circuits typically implement a logic function that represents the core of any computer or processing unit. Thus, before a logic design is constructed in real hardware, it must be tested, and the proper operation thereof has to be verified against the design specification. This task is called functional verification of a design under test (DUT) and is described in a paper by J. M. Ludden et al., entitled “Functional verification of the POWER4 microprocessor and POWER4 multiprocessor systems”, IBM Journal of Research and Development, Vol. 46, No. 1, January 2002.
Functional verification is commonly performed at various levels of abstraction of the hardware design, e.g., a switch level and a transistor level. The switch level typically includes active circuit elements (e.g., transistors) and passive circuit elements (e.g., resistors, capacitors, and inductors), whereas the transistor level includes only active devices.
In one step of the functional verification process, the hardware logic design is represented by a so-called register-transfer level (RTL) netlist, or netlist. Register transfers take place during the execution of each hardware cycle: input values are read from a set of storage elements (registers, memory cells, etc.); a computation is performed on these values; and the result is assigned to a set of storage elements. In addition to RTL netlists, gate-level netlists also exist. The gate-level is usually the result of logic synthesis methods that replace complex elements (e.g., a register) by a circuit consisting of a number of simpler elements, such as Boolean gates and latches. Direct hardware implementations in a dedicated technology are associated to such simple elements.
The netlist can be generated from a high-level description of the hardware using a standard hardware description language (HDL), such as VHDL or Verilog. Logic simulation systems use the netlist to simulate the behaviour of a DUT for a given set of input signal values. The netlist can be treated as a directed graph structure consisting of simple building blocks as nodes, and signals as connecting arcs, as described in an article by Kupriyanov et al., entitled “High Speed Event-Driven RTL Compiled Simulation”, Proc. of the 4TH. Int. Workshop on Computer Systems: Architectures, Modeling, and Simulation, 2004. The building blocks are often called boxes, and the signals, nets. Among the simple building blocks are Boolean gates, registers, arrays, latches, and black boxes representing special logical functions. In most netlist representations, the boxes and nets have a unique name by which they are identified.
Sequential logic is a type of logic circuit whose output depends not only on the present input but also on the history of the input. This is in contrast to combinatorial logic, whose output is a function of the present input. Alternatively, sequential logic stores data while combinatorial logic does not.
Functional Formal Verification (FFV)
Assuming a simple illustrative digital circuit having a plurality of 16 input signals, a plurality of 216 different input signal values exist that are to be tested for the correct operation of the circuit. However, today's hardware designs are much more complex. Even single sections of a hardware design may comprise hundreds or thousands of input signal values. In addition to the input signals, the states of internal elements of the digital circuit need to be taken into account. This enormous space of input signal values and internal states cannot be totally verified by logic simulation. Instead, regression runs of logic simulations using randomly generated values for the input signals of the DUT have been advantageously used.
A special verification technique that addresses the complete input signal value space for a DUT is referred to as functional formal verification (FFV). However, the FFV of the DUT at the register-transfer level is inherently difficult to achieve when using automated methods. Many automated functional formal verification methods are based on algorithms using Binary Decision Diagrams (BDDs) to represent the DUT, wherein a temporal logic formula is verified for a given hardware logic design. Systems implementing these methods are referred to as a (symbolic) model checker. Model checkers benefit from the fact that an RTL netlist can be represented as a finite state machine for which the complete finite state space is verified.
A temporal logic formula allows specifying the behaviour of a system over time, for example, to achieve logic design verification. Computation Tree Logic can be used to specify the signal value of a signal at predetermined discrete points in time (cycles), e.g., a signal has a value of 1 in the next cycle; a 0 in all following cycles; a 1 in at least one of the following cycles, etc. If the model checker finds a specific combination of signal values for the inputs of the netlist for which a temporal logic formula is not fulfilled, it then generates a counterexample. A counterexample is defined as a list of signals and corresponding values of either 0 or 1 in certain cycles. A model checker delivers the counterexample within a minimal number of cycles, such that the temporal logic formula is not fulfilled by the DUT.
Other automated functional formal verifications are based on algorithms that use conjunctive normal forms (CNF) to represent the hardware logic design and check whether a CNF can be satisfied (SAT) for a given hardware logic design. Systems implementing these methods are called SAT checkers. Except for special cases, attempts to formally verify a DUT result in either memory (BDD-based algorithms) or runtime (SAT-based algorithms) explosion, commonly referred to as state-space explosions (in reference to the state space of the finite state machine implemented by a DUT). Therefore, repeated attempts have been made to reduce the state space of a logic design by applying automatic transformations to the logic design. Known methods include retiming and phase-abstraction that assume logic circuits with one or more clock phases, but keeping the same type of storage elements, e.g., only edge-triggered latches or level-sensitive latches. The retiming moves storage elements within the combinatorial logic, even removes storage elements in order to reduce the state space of the logic design. However, the output signals do not change. Phase-abstraction converts storage elements of all but a single clock phase to wires, and converts the remaining storage elements into registers. For example, L1 latches are converted to wires, and L2 latches are converted to registers determined to be “hot-clocked” (clocked by an always-active clock rather than by an oscillating clock) at every clock cycle.
Another approach employs semiformal verification, a hybrid type of design exploration that moves iteratively between random simulation and a resource-bounded exhaustive search through the state space. In an article by R. M. Gott et al. entitled “Functional formal verification on designs of pSeries microprocessors and communication subsystems”, IBM J. Res. & Dev., Vol. 49, No. 4/5, 2005, are described several experiments and results for applying FFV to the design of a processor and a communication subsystem.
Design Reuse
It is well-known that the time needed to design digital circuits is a critical issue in a modern chip design. Therefore, to reuse existing hardware designs is frequently proposed as a solution to reduce this effort and reduce the time to develop a new hardware design. A typical case is to reuse an existing design that was implemented in a first semiconductor technology for its implementation in a second semiconductor technology, e.g., an improved version of the first semiconductor technology. Usually, the existing design needs to be modified for the second semiconductor technology. This step is called porting an existing design to the second semiconductor technology.
Another approach is the reuse components of a particular design for a new design. In this case, the design of existing components needs to be adapted to the new design. This step is called porting components to a new design. In such an instance, a problem often occurs when an existing and new design assume different design methodologies and a different tool set for creating the hardware. For example, a problematic case may include the use of different HDLs, such as VHDL and Verilog. Other examples of potential differences are different latch types (e.g., edge triggered vs. level sensitive latches), different clock configurations, different reset configurations, and the like.
Among other potential adaptations required when porting existing logic designs, the following typical problems can occur:                a logic function needs to be moved from one pipeline stage to the next;        the timing behaviour needs to be changed;        asynchronous resets are not allowed in the new logic design but are used in the existing logic design;        clock control signals need to be changed; and        scan path chains and associated control signals require altering.        
A simple problematic example is given by the following two HDL code fragments, one being Verilog code, the other, VHDL code:
-- VERILOG: std. asic codealways @(posedge CLK) B <= A;end;-- VHDL: IBM uproc registerport map (  nclk => CLK,  act => act,  sg => int_sg,  thold_b => reg_thold_b,  scin => int_scan(0),  scout=> int_scan(1),  din => A,  dout => C);
In the VHDL code fragment the signals act, sg, thold_b, scin, and scout are purely dedicated to clock gating and scan chains without having equivalent signals in the Verilog code fragment.
Equivalence Checking
Due to potential design errors that can be introduced in the porting step, it is usually verified in an equivalence checking step of the functional verification of a DUT, that two logic designs are equivalent. Various types of equivalence can be defined for two logic designs. Specifically, for the porting of a logic design, the cycle-accurate equivalence needs to be verified, wherein when starting from reset, a first logic design produces identical outputs as a second design for every clock cycle upon applying equal inputs. In the remainder equivalence of digital circuits means, cycle-accurate equivalence and equivalence checking is the process that verifies the equivalence.
For the equivalence checking of two logic designs comprising combinatorial logic only, powerful tools are available on the market. These tools are referred to as Boolean equivalence checkers and are mainly used to verify that two gate-level netlists are equivalent, where the gate-level netlists are the result from automatic logic design transformation steps of a logic design at the RTL.
A common case is the logic synthesis step that automatically transforms the logic design from an RTL description to a gate-level netlist. This automatic transformation is related to constraints of the semiconductor technology used to implement the logic design. Following logic synthesis, the resulting gate-level netlist is verified to determine whether it is equivalent to the RTL description. Potentially, a Boolean equivalence checker automatically transforms the RTL netlist to an internal gate-level netlist. Since it is assumed that the logic synthesis does not modify the storage elements of the RTL netlist, only the combinatorial logic part of the netlists needs to be verified. Combinatorial logic parts can be extracted automatically from the netlists by the Boolean equivalence checker.
Boolean equivalence checkers perform the equivalence checking such that they combine the two netlists in a single gate-level netlist with the same set of inputs, each of which is verified by formal verification techniques, i.e., every possible combination of inputs is verified that the corresponding outputs of the two designs are equal. Often Boolean equivalence checkers are implemented using BDDs.
Available tools which can perform the equivalence checking of two logic designs at the RTL that includes sequential logic circuits face the problem of a potentially huge state space of a finite state machine represented by the logic designs. This problem either restricts the verification coverage that can be achieved or it prevents the use of the so-called sequential equivalence checker tools in many real-world porting scenarios. Many sequential equivalence checker tools are based on FFV tools, e.g., model checkers. But also semiformal verification methods can be used to implement sequential equivalence checkers.
Boolean and sequential equivalence checking methods for logic designs used for real-world logic designs assume an equal set of inputs and outputs of the two logic designs that are compared. However, as described above, this is often not the case for logic designs ported from one semiconductor node to another and for reusing logic design components. Therefore, there is a need in industry for existing formal verification methods that apply to sequential equivalence checking of digital circuit designs.